package kodkod.analysis.ordering;

import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.text.NumberFormat;

import kodkod.analysis.OrderableSolver;
import kodkod.ast.Relation;
import kodkod.engine.fol2sat.Translation;

public class UniformPromotion extends AbstractOrdering {
	
	double weight = 1.0;

	public UniformPromotion() {
		this(1.0);
	}
	
	public UniformPromotion(double weight) {
		super();
		this.weight = weight;
	}
	
	public void apply(Translation translation) {
		for (int pos = 0, n = translation.primaryRelations.size(); pos < n; pos++) {
			Relation rel = translation.primaryRelations.get(pos);
			int[] vars = translation.primaryVariables(rel).toArray();
			
			for (int var : vars) {
				weightVariable((OrderableSolver)translation.cnf(), var, weight);
			}
		}
	}
	
	public String toString() {
		if (softOrder) {
			StringBuffer buf = new StringBuffer();
			buf.append("UniformInitialize");
			DecimalFormatSymbols symbols = new DecimalFormatSymbols();
			symbols.setDecimalSeparator('.');
			NumberFormat format = new DecimalFormat("#0.00", symbols);
			buf.append("-");
			buf.append(format.format(weight));
			return buf.toString();
		} else {
			return "UniformOverride";
		}
	}
}
